Nuprl Lemma : bor_tt_simp
12,41
postcript
pdf
u
:
. (
u
tt) = tt
latex
ProofTree
Definitions
t
T
Lemmas
bool
wf
,
btrue
wf
origin
u:
. (u 
tt) = tt 
u:. (u tt) = tt
T